﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;

namespace CodeContracts
{
    public class Calculator : IDemoInterface
    {
        private int result;
        
        // Without Code Contracts
        public int Add_Old(int operand1, int operand2)
        {
            if (operand1 < 0)
            {
                throw new ArgumentException("First operand cannot be less than 0");
            }
            if (operand2 < 0)
            {
                throw new ArgumentException("Second operand cannot be less than 0");
            }
            Contract.EndContractBlock();

            result = operand1 + operand2;

            return result;
        }

        // With Code Contracts
        public int Add(int operand1, int operand2)
        {
            Contract.Requires<ArgumentException>(operand1 >= 0);
            Contract.Requires<ArgumentException>(operand2 >= 0);
            Contract.Requires(operand1 + operand2 > 0);
            //Contract.Requires(operand1 + operand2 < 10000);
            Contract.Ensures(Contract.Result<int>() >= 0);

            result = operand1 + operand2;

            return result;
        }

        [ContractInvariantMethod]
        private void ResultRange()
        {
            Contract.Invariant(this.result >= 0);
            Contract.Invariant(this.result < 10000);
        }

        public bool IsString(string check)
        {
            //Contract.Requires(string.IsNullOrWhiteSpace(check) == false);

            return true;
        }
    }
}
